So, we have a semantics, we have a formal language, what do we still need?

For logic.

Different rules?

What kind of rules?

To substitute operators and variables to new?

We call those things a calculus.

Yeah.

All together.

Yes, but you're right.

We need a calculus and preferably a sound and complete one.

Before we can build one, let us go back to the only innovation.

If you look at the whole thing, then everything but the last line looks exactly like propositional

logic with the one difference that instead of having simple propositional variables in

this case, we have complex atomic formulae.

Everything else?

Dead simple.

And you remember that we wrote down Peter loves Mary, then Peter and John love whatever,

I don't remember, right?

We really used a version of propositional logic that was just missing this last line

which gives us quantifiers.

And that's the logic I normally call PL and Q which is predicate logic, no quantifiers.

And it turns out that this is just propositional logic.

If you miss out on the quantifiers, you have propositional logic.

We know exactly what we have to do for propositional logic, so the only thing we have to really

wrap our heads around is what do we do with that?

Okay?

Well, this kind of already tells us what we want to do this, what we want to do here.

Whenever we see a for all XA, we want to vary X, the values of X, over everything we know.

And the only thing we really know in first-order logic, i.e. syntactically can write down,

is the terms.

So instead of semantically varying over all the values here, we value over all these syntactic

individuals.

And that operation, sticking a syntactic individual for a variable, we call substitution which

is exactly what we're going to look at now.

Okay?

So what is a substitution?

A substitution is something of the form Z for Y, Y for X, and so on.

You have an assignment to variables, an assignment of terms for variables.

And we'll write them some kind of a term A1 for X1 up to An for Xn.

That's what a substitution looks like.

And I can apply it to a term by just replacing variables.

So if I have something of the form F of X, G of Y, H of X, Y, Z, two brackets, and I

apply A for X, F of A for Z to this term, then that means replace all the Xs by A and

all the Zs by F of A.

So I have an X here, so we have an F of A, G of Y, because we are not replacing Y, and

H of A, Y, F of A.

Yeah, that's enough.

Okay?

Dead easy, one would think.

It's not quite as easy.